\begin{tabbing}
ecl{-}es{-}halt(${\it es}$; $x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$ecl\_ind(\=$x$;\+
\\[0ex]$k$,${\it test}$.($\lambda$$n$,$e_{1}$,$e_{2}$. if ($n$ =$_{0}$ 0)
\\[0ex]then \=$e_{2}$ = \+
\\[0ex]first $e$ $\geq$ $e_{1}$.\=(es{-}kind(${\it es}$; $e$) = $k$)\+
\\[0ex]c$\wedge$ ($\uparrow$(${\it test}$(es{-}state{-}when(${\it es}$; $e$),es{-}val(${\it es}$; $e$))))
\-\-\\[0ex]else False
\\[0ex]fi );
\\[0ex]$a$,$b$,${\it ha}$,${\it hb}$.($\lambda$$n$,$e_{1}$,$e_{2}$. if ($n$ =$_{0}$ 0) then False else ${\it ha}$($n$,$e_{1}$,$e_{2}$) fi 
\\[0ex]$\vee$ $\exists$$e$$\in$($e_{1}$,$e_{2}$].(${\it ha}$(0,$e_{1}$,es{-}pred(${\it es}$; $e$))) $\wedge$ (${\it hb}$($n$,$e$,$e_{2}$)));
\\[0ex]$a$,$b$,${\it ha}$,${\it hb}$.($\lambda$$n$,$e_{1}$,$e_{2}$. if ($n$ =$_{0}$ 0)
\\[0ex]then \=((${\it ha}$(0,$e_{1}$,$e_{2}$)) $\wedge$ $\exists$$e$$\in$[$e_{1}$,$e_{2}$].${\it hb}$(0,$e_{1}$,$e$))\+
\\[0ex]$\vee$ ((${\it hb}$(0,$e_{1}$,$e_{2}$)) $\wedge$ $\exists$$e$$\in$[$e_{1}$,$e_{2}$].${\it ha}$(0,$e_{1}$,$e$))
\-\\[0ex]else \=((${\it ha}$($n$,$e_{1}$,$e_{2}$))\+
\\[0ex]$\wedge$ l{-}all(\=cons(0; ecl{-}ex($b$));\+
\\[0ex]$m$.if $n$ $\leq$z $m$
\\[0ex]then $\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$(${\it hb}$($m$,$e_{1}$,$e$))
\\[0ex]else $\forall$$e$$\in$[$e_{1}$,$e_{2}$].$\neg$(${\it hb}$($m$,$e_{1}$,$e$))
\\[0ex]fi ))
\-\\[0ex]$\vee$ \=((${\it hb}$($n$,$e_{1}$,$e_{2}$))\+
\\[0ex]$\wedge$ l{-}all(\=cons(0; ecl{-}ex($a$));\+
\\[0ex]$m$.if $n$ $\leq$z $m$
\\[0ex]then $\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$(${\it ha}$($m$,$e_{1}$,$e$))
\\[0ex]else $\forall$$e$$\in$[$e_{1}$,$e_{2}$].$\neg$(${\it ha}$($m$,$e_{1}$,$e$))
\\[0ex]fi ))
\-\-\-\\[0ex]fi );
\\[0ex]$a$,$b$,${\it ha}$,${\it hb}$.($\lambda$$n$,$e_{1}$,$e_{2}$. ((${\it ha}$($n$,$e_{1}$,$e_{2}$))
\\[0ex]$\wedge$ l{-}all(\=cons(0; ecl{-}ex($b$));\+
\\[0ex]$m$.if $n$ $\leq$z $m$
\\[0ex]then $\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$(${\it hb}$($m$,$e_{1}$,$e$))
\\[0ex]else $\forall$$e$$\in$[$e_{1}$,$e_{2}$].$\neg$(${\it hb}$($m$,$e_{1}$,$e$))
\\[0ex]fi ))
\-\\[0ex]$\vee$ \=((${\it hb}$($n$,$e_{1}$,$e_{2}$))\+
\\[0ex]$\wedge$ l{-}all(\=cons(0; ecl{-}ex($a$));\+
\\[0ex]$m$.if $n$ $\leq$z $m$
\\[0ex]then $\forall$$e$$\in$[$e_{1}$,$e_{2}$).$\neg$(${\it ha}$($m$,$e_{1}$,$e$))
\\[0ex]else $\forall$$e$$\in$[$e_{1}$,$e_{2}$].$\neg$(${\it ha}$($m$,$e_{1}$,$e$))
\\[0ex]fi )));
\-\-\\[0ex]$a$,${\it ha}$.($\lambda$$n$,$e_{1}$,$e_{2}$. if ($n$ =$_{0}$ 0)
\\[0ex]then False
\\[0ex]else [$e_{1}$;$e_{2}$]$\sim$([$x$,$y$].${\it ha}$(0,$x$,$y$))$\ast$[$x$,$y$].${\it ha}$($n$,$x$,$y$)
\\[0ex]fi );
\\[0ex]$a$,$m$,${\it ha}$.${\it ha}$;
\\[0ex]$a$,$m$,${\it ha}$.($\lambda$$n$,$e_{1}$,$e_{2}$. if ($n$ =$_{0}$ 0) then False else ${\it ha}$($n$,$e_{1}$,$e_{2}$) fi 
\\[0ex]$\vee$ if ($n$ =$_{0}$ $m$) then ${\it ha}$(0,$e_{1}$,$e_{2}$) else False fi );
\\[0ex]$a$,$l$,${\it ha}$.($\lambda$$n$,$e_{1}$,$e_{2}$. ((${\it ha}$($n$,$e_{1}$,$e_{2}$)) $\wedge$ ($\neg$($n$ $\in$ $l$)))
\\[0ex]$\vee$ if ($n$ =$_{0}$ 0) then l\_exists($l$; $\mathbb{N}$; $m$.(${\it ha}$($m$,$e_{1}$,$e_{2}$))) else False fi ))
\-
\end{tabbing}